T:Type, l1,l2:(T List). (append(l1; l2) = []  (T List))  ((l1 = [])  (l2 = [])) 

latex

Definitions	prop{i:l}, t  T, P  Q, x:A. B(x), P  Q, Y, P  Q, append(as; bs), P  Q, ||as||, False
Lemmas	non neg length, length wf1, append wf